L, L':( List). (0 < ||L||)  l_subset(;L;L')  (imax-list(L)  imax-list(L')) 

latex

Definitions	||as||, , a < b, Void, x:AB(x), xL. P(x), P  Q, False, A, A  B, t  T, x:A. B(x), imax-list(L), P  Q, P & Q, P  Q, type List, #$n, , l_subset(T;as;bs), s = t, (x  l), x:A  B(x), P  Q, i  j , [car / cdr], (xL.P(x)), x:A. B(x)
Lemmas	le wf, imax-list-ub, length cons, non neg length, cons member, l member wf, nil member, l subset wf, length wf1, imax-list-lb, imax-list wf